Termination Proof Script

• Consider the SCC {8}. There are no usable rules. By taking the AF π with π(F) = 1 together with the lexicographic path order with empty precedence, rule 8 is strictly decreasing.


• Consider the SCC {9,10,13}. By taking the AF π with π(if) = 1, π(g) = π(G) = 2 and π(f) = π(s) = [ ] together with the lexicographic path order with precedence c ≻ f ≻ false ≻ s and f ≻ true ≻ s, the rules in {3,6} are weakly decreasing and the rules in {1,2,4,5,7,9,10,13} are strictly decreasing.